ecase1($e$;${\it info}$;$i$.$f$($i$);$l$,${\it e'}$.$g$($l$;${\it e'}$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case ${\it info}$($e$) of inl($p$) =$>$ $f$($p$.1) $\mid$ inr($q$) =$>$ $g$($q$.1.1;($q$.1).2)